YES 2.611
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/FiniteMap.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ BR
mainModule FiniteMap
| ((lookupFM :: FiniteMap Int a -> Int -> Maybe a) :: FiniteMap Int a -> Int -> Maybe a) |
module FiniteMap where
| import qualified Maybe import qualified Prelude
|
| data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b)
|
| instance (Eq a, Eq b) => Eq (FiniteMap b a) where
|
| lookupFM :: Ord b => FiniteMap b a -> b -> Maybe a
lookupFM | EmptyFM key | = | Nothing |
lookupFM | (Branch key elt _ fm_l fm_r) key_to_find | |
| | key_to_find < key | = |
lookupFM fm_l key_to_find |
|
| | key_to_find > key | = |
lookupFM fm_r key_to_find |
|
| | otherwise | = |
|
|
|
module Maybe where
| import qualified FiniteMap import qualified Prelude
|
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule FiniteMap
| ((lookupFM :: FiniteMap Int a -> Int -> Maybe a) :: FiniteMap Int a -> Int -> Maybe a) |
module FiniteMap where
| import qualified Maybe import qualified Prelude
|
| data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b)
|
| instance (Eq a, Eq b) => Eq (FiniteMap a b) where
|
| lookupFM :: Ord a => FiniteMap a b -> a -> Maybe b
lookupFM | EmptyFM key | = | Nothing |
lookupFM | (Branch key elt vw fm_l fm_r) key_to_find | |
| | key_to_find < key | = |
lookupFM fm_l key_to_find |
|
| | key_to_find > key | = |
lookupFM fm_r key_to_find |
|
| | otherwise | = |
|
|
|
module Maybe where
| import qualified FiniteMap import qualified Prelude
|
Cond Reductions:
The following Function with conditions
lookupFM | EmptyFM key | = Nothing |
lookupFM | (Branch key elt vw fm_l fm_r) key_to_find |
| | key_to_find < key |
= | lookupFM fm_l key_to_find |
|
| | key_to_find > key |
= | lookupFM fm_r key_to_find |
|
| | otherwise | |
|
is transformed to
lookupFM | EmptyFM key | = lookupFM4 EmptyFM key |
lookupFM | (Branch key elt vw fm_l fm_r) key_to_find | = lookupFM3 (Branch key elt vw fm_l fm_r) key_to_find |
lookupFM2 | key elt vw fm_l fm_r key_to_find True | = lookupFM fm_l key_to_find |
lookupFM2 | key elt vw fm_l fm_r key_to_find False | = lookupFM1 key elt vw fm_l fm_r key_to_find (key_to_find > key) |
lookupFM1 | key elt vw fm_l fm_r key_to_find True | = lookupFM fm_r key_to_find |
lookupFM1 | key elt vw fm_l fm_r key_to_find False | = lookupFM0 key elt vw fm_l fm_r key_to_find otherwise |
lookupFM0 | key elt vw fm_l fm_r key_to_find True | = Just elt |
lookupFM3 | (Branch key elt vw fm_l fm_r) key_to_find | = lookupFM2 key elt vw fm_l fm_r key_to_find (key_to_find < key) |
lookupFM4 | EmptyFM key | = Nothing |
lookupFM4 | wv ww | = lookupFM3 wv ww |
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule FiniteMap
| (lookupFM :: FiniteMap Int a -> Int -> Maybe a) |
module FiniteMap where
| import qualified Maybe import qualified Prelude
|
| data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b)
|
| instance (Eq a, Eq b) => Eq (FiniteMap b a) where
|
| lookupFM :: Ord b => FiniteMap b a -> b -> Maybe a
lookupFM | EmptyFM key | = | lookupFM4 EmptyFM key |
lookupFM | (Branch key elt vw fm_l fm_r) key_to_find | = | lookupFM3 (Branch key elt vw fm_l fm_r) key_to_find |
|
|
lookupFM0 | key elt vw fm_l fm_r key_to_find True | = | Just elt |
|
|
lookupFM1 | key elt vw fm_l fm_r key_to_find True | = | lookupFM fm_r key_to_find |
lookupFM1 | key elt vw fm_l fm_r key_to_find False | = | lookupFM0 key elt vw fm_l fm_r key_to_find otherwise |
|
|
lookupFM2 | key elt vw fm_l fm_r key_to_find True | = | lookupFM fm_l key_to_find |
lookupFM2 | key elt vw fm_l fm_r key_to_find False | = | lookupFM1 key elt vw fm_l fm_r key_to_find (key_to_find > key) |
|
|
lookupFM3 | (Branch key elt vw fm_l fm_r) key_to_find | = | lookupFM2 key elt vw fm_l fm_r key_to_find (key_to_find < key) |
|
|
lookupFM4 | EmptyFM key | = | Nothing |
lookupFM4 | wv ww | = | lookupFM3 wv ww |
|
module Maybe where
| import qualified FiniteMap import qualified Prelude
|
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
new_lookupFM2(wx108, wx109, wx110, wx111, wx112, wx113, Zero, Zero, h) → new_lookupFM20(wx108, wx109, wx110, wx111, wx112, wx113, h)
new_lookupFM(Branch(Pos(Succ(wx3000)), wx31, wx32, wx33, wx34), Pos(Zero), bb) → new_lookupFM(wx33, Pos(Zero), bb)
new_lookupFM20(wx108, wx109, wx110, wx111, wx112, wx113, h) → new_lookupFM1(wx108, wx109, wx110, wx111, wx112, wx113, Succ(wx113), Succ(wx108), h)
new_lookupFM1(wx228, wx229, wx230, wx231, wx232, wx233, Succ(wx2340), Zero, ba) → new_lookupFM(wx232, Pos(Succ(wx233)), ba)
new_lookupFM(Branch(Pos(Succ(wx3000)), wx31, wx32, wx33, wx34), Pos(Succ(wx400)), bb) → new_lookupFM2(wx3000, wx31, wx32, wx33, wx34, wx400, wx400, wx3000, bb)
new_lookupFM(Branch(Neg(wx300), wx31, wx32, wx33, wx34), Pos(Succ(wx400)), bb) → new_lookupFM(wx34, Pos(Succ(wx400)), bb)
new_lookupFM21(wx117, wx118, wx119, wx120, wx121, wx122, Zero, Zero, bc) → new_lookupFM22(wx117, wx118, wx119, wx120, wx121, wx122, bc)
new_lookupFM21(wx117, wx118, wx119, wx120, wx121, wx122, Succ(wx1230), Succ(wx1240), bc) → new_lookupFM21(wx117, wx118, wx119, wx120, wx121, wx122, wx1230, wx1240, bc)
new_lookupFM(Branch(Neg(Succ(wx3000)), wx31, wx32, wx33, wx34), Pos(Zero), bb) → new_lookupFM(wx34, Pos(Zero), bb)
new_lookupFM(Branch(Neg(Succ(wx3000)), wx31, wx32, wx33, wx34), Neg(Succ(wx400)), bb) → new_lookupFM21(wx3000, wx31, wx32, wx33, wx34, wx400, wx3000, wx400, bb)
new_lookupFM22(wx117, wx118, wx119, wx120, wx121, wx122, bc) → new_lookupFM10(wx117, wx118, wx119, wx120, wx121, wx122, Succ(wx117), Succ(wx122), bc)
new_lookupFM(Branch(Neg(Zero), wx31, wx32, wx33, wx34), Neg(Succ(wx400)), bb) → new_lookupFM(wx33, Neg(Succ(wx400)), bb)
new_lookupFM1(wx228, wx229, wx230, wx231, wx232, wx233, Succ(wx2340), Succ(wx2350), ba) → new_lookupFM1(wx228, wx229, wx230, wx231, wx232, wx233, wx2340, wx2350, ba)
new_lookupFM2(wx108, wx109, wx110, wx111, wx112, wx113, Succ(wx1140), Succ(wx1150), h) → new_lookupFM2(wx108, wx109, wx110, wx111, wx112, wx113, wx1140, wx1150, h)
new_lookupFM(Branch(Pos(wx300), wx31, wx32, wx33, wx34), Neg(Succ(wx400)), bb) → new_lookupFM(wx33, Neg(Succ(wx400)), bb)
new_lookupFM10(wx237, wx238, wx239, wx240, wx241, wx242, Succ(wx2430), Succ(wx2440), bd) → new_lookupFM10(wx237, wx238, wx239, wx240, wx241, wx242, wx2430, wx2440, bd)
new_lookupFM2(wx108, wx109, wx110, wx111, wx112, wx113, Zero, Succ(wx1150), h) → new_lookupFM(wx111, Pos(Succ(wx113)), h)
new_lookupFM(Branch(Pos(Succ(wx3000)), wx31, wx32, wx33, wx34), Neg(Zero), bb) → new_lookupFM(wx33, Neg(Zero), bb)
new_lookupFM21(wx117, wx118, wx119, wx120, wx121, wx122, Zero, Succ(wx1240), bc) → new_lookupFM(wx120, Neg(Succ(wx122)), bc)
new_lookupFM2(wx108, wx109, wx110, wx111, wx112, wx113, Succ(wx1140), Zero, h) → new_lookupFM1(wx108, wx109, wx110, wx111, wx112, wx113, Succ(wx113), Succ(wx108), h)
new_lookupFM(Branch(Pos(Zero), wx31, wx32, wx33, wx34), Pos(Succ(wx400)), bb) → new_lookupFM(wx34, Pos(Succ(wx400)), bb)
new_lookupFM21(wx117, wx118, wx119, wx120, wx121, wx122, Succ(wx1230), Zero, bc) → new_lookupFM10(wx117, wx118, wx119, wx120, wx121, wx122, Succ(wx117), Succ(wx122), bc)
new_lookupFM10(wx237, wx238, wx239, wx240, wx241, wx242, Succ(wx2430), Zero, bd) → new_lookupFM(wx241, Neg(Succ(wx242)), bd)
new_lookupFM(Branch(Neg(Succ(wx3000)), wx31, wx32, wx33, wx34), Neg(Zero), bb) → new_lookupFM(wx34, Neg(Zero), bb)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 4 SCCs.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_lookupFM(Branch(Pos(Succ(wx3000)), wx31, wx32, wx33, wx34), Neg(Zero), bb) → new_lookupFM(wx33, Neg(Zero), bb)
new_lookupFM(Branch(Neg(Succ(wx3000)), wx31, wx32, wx33, wx34), Neg(Zero), bb) → new_lookupFM(wx34, Neg(Zero), bb)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_lookupFM(Branch(Neg(Succ(wx3000)), wx31, wx32, wx33, wx34), Neg(Zero), bb) → new_lookupFM(wx34, Neg(Zero), bb)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3
- new_lookupFM(Branch(Pos(Succ(wx3000)), wx31, wx32, wx33, wx34), Neg(Zero), bb) → new_lookupFM(wx33, Neg(Zero), bb)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_lookupFM(Branch(Pos(wx300), wx31, wx32, wx33, wx34), Neg(Succ(wx400)), bb) → new_lookupFM(wx33, Neg(Succ(wx400)), bb)
new_lookupFM10(wx237, wx238, wx239, wx240, wx241, wx242, Succ(wx2430), Succ(wx2440), bd) → new_lookupFM10(wx237, wx238, wx239, wx240, wx241, wx242, wx2430, wx2440, bd)
new_lookupFM21(wx117, wx118, wx119, wx120, wx121, wx122, Succ(wx1230), Succ(wx1240), bc) → new_lookupFM21(wx117, wx118, wx119, wx120, wx121, wx122, wx1230, wx1240, bc)
new_lookupFM21(wx117, wx118, wx119, wx120, wx121, wx122, Zero, Zero, bc) → new_lookupFM22(wx117, wx118, wx119, wx120, wx121, wx122, bc)
new_lookupFM21(wx117, wx118, wx119, wx120, wx121, wx122, Zero, Succ(wx1240), bc) → new_lookupFM(wx120, Neg(Succ(wx122)), bc)
new_lookupFM(Branch(Neg(Succ(wx3000)), wx31, wx32, wx33, wx34), Neg(Succ(wx400)), bb) → new_lookupFM21(wx3000, wx31, wx32, wx33, wx34, wx400, wx3000, wx400, bb)
new_lookupFM21(wx117, wx118, wx119, wx120, wx121, wx122, Succ(wx1230), Zero, bc) → new_lookupFM10(wx117, wx118, wx119, wx120, wx121, wx122, Succ(wx117), Succ(wx122), bc)
new_lookupFM(Branch(Neg(Zero), wx31, wx32, wx33, wx34), Neg(Succ(wx400)), bb) → new_lookupFM(wx33, Neg(Succ(wx400)), bb)
new_lookupFM10(wx237, wx238, wx239, wx240, wx241, wx242, Succ(wx2430), Zero, bd) → new_lookupFM(wx241, Neg(Succ(wx242)), bd)
new_lookupFM22(wx117, wx118, wx119, wx120, wx121, wx122, bc) → new_lookupFM10(wx117, wx118, wx119, wx120, wx121, wx122, Succ(wx117), Succ(wx122), bc)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_lookupFM10(wx237, wx238, wx239, wx240, wx241, wx242, Succ(wx2430), Succ(wx2440), bd) → new_lookupFM10(wx237, wx238, wx239, wx240, wx241, wx242, wx2430, wx2440, bd)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 > 7, 8 > 8, 9 >= 9
- new_lookupFM21(wx117, wx118, wx119, wx120, wx121, wx122, Zero, Zero, bc) → new_lookupFM22(wx117, wx118, wx119, wx120, wx121, wx122, bc)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 9 >= 7
- new_lookupFM10(wx237, wx238, wx239, wx240, wx241, wx242, Succ(wx2430), Zero, bd) → new_lookupFM(wx241, Neg(Succ(wx242)), bd)
The graph contains the following edges 5 >= 1, 9 >= 3
- new_lookupFM21(wx117, wx118, wx119, wx120, wx121, wx122, Succ(wx1230), Zero, bc) → new_lookupFM10(wx117, wx118, wx119, wx120, wx121, wx122, Succ(wx117), Succ(wx122), bc)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 9 >= 9
- new_lookupFM22(wx117, wx118, wx119, wx120, wx121, wx122, bc) → new_lookupFM10(wx117, wx118, wx119, wx120, wx121, wx122, Succ(wx117), Succ(wx122), bc)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 >= 9
- new_lookupFM(Branch(Neg(Succ(wx3000)), wx31, wx32, wx33, wx34), Neg(Succ(wx400)), bb) → new_lookupFM21(wx3000, wx31, wx32, wx33, wx34, wx400, wx3000, wx400, bb)
The graph contains the following edges 1 > 1, 1 > 2, 1 > 3, 1 > 4, 1 > 5, 2 > 6, 1 > 7, 2 > 8, 3 >= 9
- new_lookupFM21(wx117, wx118, wx119, wx120, wx121, wx122, Zero, Succ(wx1240), bc) → new_lookupFM(wx120, Neg(Succ(wx122)), bc)
The graph contains the following edges 4 >= 1, 9 >= 3
- new_lookupFM21(wx117, wx118, wx119, wx120, wx121, wx122, Succ(wx1230), Succ(wx1240), bc) → new_lookupFM21(wx117, wx118, wx119, wx120, wx121, wx122, wx1230, wx1240, bc)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 > 7, 8 > 8, 9 >= 9
- new_lookupFM(Branch(Neg(Zero), wx31, wx32, wx33, wx34), Neg(Succ(wx400)), bb) → new_lookupFM(wx33, Neg(Succ(wx400)), bb)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3
- new_lookupFM(Branch(Pos(wx300), wx31, wx32, wx33, wx34), Neg(Succ(wx400)), bb) → new_lookupFM(wx33, Neg(Succ(wx400)), bb)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_lookupFM(Branch(Pos(Succ(wx3000)), wx31, wx32, wx33, wx34), Pos(Zero), bb) → new_lookupFM(wx33, Pos(Zero), bb)
new_lookupFM(Branch(Neg(Succ(wx3000)), wx31, wx32, wx33, wx34), Pos(Zero), bb) → new_lookupFM(wx34, Pos(Zero), bb)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_lookupFM(Branch(Neg(Succ(wx3000)), wx31, wx32, wx33, wx34), Pos(Zero), bb) → new_lookupFM(wx34, Pos(Zero), bb)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3
- new_lookupFM(Branch(Pos(Succ(wx3000)), wx31, wx32, wx33, wx34), Pos(Zero), bb) → new_lookupFM(wx33, Pos(Zero), bb)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_lookupFM2(wx108, wx109, wx110, wx111, wx112, wx113, Succ(wx1140), Succ(wx1150), h) → new_lookupFM2(wx108, wx109, wx110, wx111, wx112, wx113, wx1140, wx1150, h)
new_lookupFM1(wx228, wx229, wx230, wx231, wx232, wx233, Succ(wx2340), Succ(wx2350), ba) → new_lookupFM1(wx228, wx229, wx230, wx231, wx232, wx233, wx2340, wx2350, ba)
new_lookupFM2(wx108, wx109, wx110, wx111, wx112, wx113, Zero, Zero, h) → new_lookupFM20(wx108, wx109, wx110, wx111, wx112, wx113, h)
new_lookupFM1(wx228, wx229, wx230, wx231, wx232, wx233, Succ(wx2340), Zero, ba) → new_lookupFM(wx232, Pos(Succ(wx233)), ba)
new_lookupFM20(wx108, wx109, wx110, wx111, wx112, wx113, h) → new_lookupFM1(wx108, wx109, wx110, wx111, wx112, wx113, Succ(wx113), Succ(wx108), h)
new_lookupFM(Branch(Neg(wx300), wx31, wx32, wx33, wx34), Pos(Succ(wx400)), bb) → new_lookupFM(wx34, Pos(Succ(wx400)), bb)
new_lookupFM2(wx108, wx109, wx110, wx111, wx112, wx113, Zero, Succ(wx1150), h) → new_lookupFM(wx111, Pos(Succ(wx113)), h)
new_lookupFM(Branch(Pos(Succ(wx3000)), wx31, wx32, wx33, wx34), Pos(Succ(wx400)), bb) → new_lookupFM2(wx3000, wx31, wx32, wx33, wx34, wx400, wx400, wx3000, bb)
new_lookupFM2(wx108, wx109, wx110, wx111, wx112, wx113, Succ(wx1140), Zero, h) → new_lookupFM1(wx108, wx109, wx110, wx111, wx112, wx113, Succ(wx113), Succ(wx108), h)
new_lookupFM(Branch(Pos(Zero), wx31, wx32, wx33, wx34), Pos(Succ(wx400)), bb) → new_lookupFM(wx34, Pos(Succ(wx400)), bb)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_lookupFM1(wx228, wx229, wx230, wx231, wx232, wx233, Succ(wx2340), Succ(wx2350), ba) → new_lookupFM1(wx228, wx229, wx230, wx231, wx232, wx233, wx2340, wx2350, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 > 7, 8 > 8, 9 >= 9
- new_lookupFM2(wx108, wx109, wx110, wx111, wx112, wx113, Zero, Zero, h) → new_lookupFM20(wx108, wx109, wx110, wx111, wx112, wx113, h)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 9 >= 7
- new_lookupFM1(wx228, wx229, wx230, wx231, wx232, wx233, Succ(wx2340), Zero, ba) → new_lookupFM(wx232, Pos(Succ(wx233)), ba)
The graph contains the following edges 5 >= 1, 9 >= 3
- new_lookupFM2(wx108, wx109, wx110, wx111, wx112, wx113, Succ(wx1140), Zero, h) → new_lookupFM1(wx108, wx109, wx110, wx111, wx112, wx113, Succ(wx113), Succ(wx108), h)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 9 >= 9
- new_lookupFM20(wx108, wx109, wx110, wx111, wx112, wx113, h) → new_lookupFM1(wx108, wx109, wx110, wx111, wx112, wx113, Succ(wx113), Succ(wx108), h)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 >= 9
- new_lookupFM(Branch(Pos(Succ(wx3000)), wx31, wx32, wx33, wx34), Pos(Succ(wx400)), bb) → new_lookupFM2(wx3000, wx31, wx32, wx33, wx34, wx400, wx400, wx3000, bb)
The graph contains the following edges 1 > 1, 1 > 2, 1 > 3, 1 > 4, 1 > 5, 2 > 6, 2 > 7, 1 > 8, 3 >= 9
- new_lookupFM2(wx108, wx109, wx110, wx111, wx112, wx113, Zero, Succ(wx1150), h) → new_lookupFM(wx111, Pos(Succ(wx113)), h)
The graph contains the following edges 4 >= 1, 9 >= 3
- new_lookupFM2(wx108, wx109, wx110, wx111, wx112, wx113, Succ(wx1140), Succ(wx1150), h) → new_lookupFM2(wx108, wx109, wx110, wx111, wx112, wx113, wx1140, wx1150, h)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 > 7, 8 > 8, 9 >= 9
- new_lookupFM(Branch(Neg(wx300), wx31, wx32, wx33, wx34), Pos(Succ(wx400)), bb) → new_lookupFM(wx34, Pos(Succ(wx400)), bb)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3
- new_lookupFM(Branch(Pos(Zero), wx31, wx32, wx33, wx34), Pos(Succ(wx400)), bb) → new_lookupFM(wx34, Pos(Succ(wx400)), bb)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3